a:, n:. (a rem n) = (a rem -n) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), i  j , , P  Q, P & Q, P  Q, P  Q, , False, A  B, {...i}, A, , P  Q, Dec(P), , a  b  T
Lemmas	nat plus wf, decidable le, rem 4 to 1, le wf, rem 3 to 1, rem 2 to 1, int nzero wf